时间到了十九世纪末，康托、布尔、弗雷格、希尔伯特、罗素、布劳威、哥德尔等人定义了形式化逻辑的符号系统。而「证明」则是在利用形式化逻辑的符号语言编写的推理过程。逻辑本身靠谱么？逻辑本身「自恰」吗？逻辑推理本身对不对，能够证明吗？这让 数学家/逻辑学家/计算机科学家 发明（发现） 了符号系统，语法 vs. 语义，可靠 vs. 完备，递归 vs. 无穷。（这部分精彩故事请参看『逻辑的引擎』一书[3]）。1910年，罗素发表了洪(zhuan)荒(tou)巨著『数学原理』。在书中，罗素与怀特海试图将数学完整地「形式化」下来。如果能达到这样的目标，所有的数学成果都将以证明的方式建立在坚实的基础上。下图就是『数学原理（卷二）』中的一页：
上面例子就是一个「交互式证明」。假设Alice知道方程的解， f(w) = 0，那么 Alice 如何让 Bob 确信她知道 w 呢？Alice 在 「黑科技阶段」 告诉了 Bob 一大堆的信息。好了，关键问题是，Bob 能不能从 Alice 所说的一大堆信息中猜出w 到底是几，或者能分析出关于 w 的蛛丝马迹呢？如果 Bob 有这个能力，Bob也许就没必要掏钱了，因为他已经获得了这个值钱的信息。 请注意，如果 Alice 与 Bob 的对话是 「零知识」 的，那么 Bob 除了知道 w 是 f(w)=0 的解之外，不能获取其它任何关于 w 的信息。这一点非常重要，这是保护 Alice 的利益。现在回顾一下「零知识证明」这个词，英文叫 「Zero-Knowledge Proof」 。这个词包含三个关键部分：
现在 Alice 想证明给 Bob 她有答案，但是又不想让 Bob 知道这个答案。Alice 要怎么做呢？Alice 先要对染过色的图进行一些「变换」，把颜色做一次大挪移，例如把所有的绿色变成橙色，把所有的蓝色变成绿色，把所有的绿色变成橙色。然后 Alice 得到了一个新的染色答案，这时候她把新的图的每一个顶点都用纸片盖上，然后出示给 Bob 看。
看下图，这时候 Bob 要出手了（请见下图），他要随机挑选一条「边」，注意是随机，不让 Alice 提前预测到的随机数。
假设 Bob 挑选的是最下面的一条边，然后告诉 Alice。
这时候 Alice 揭开这条边两端的纸片，让 Bob 检查，Bob 发现这两个顶点的颜色是不同的，那么 Bob 认为这次检验同构。这时候，Bob 只看到了图的局部，能被说服剩下的图顶点的染色都没问题吗？你肯定觉得这远远不够，也许恰好 Alice 蒙对了呢？其它没暴露的顶点可能是胡乱染色的。没关系，Bob 可以要求 Alice 再来一遍，看下图
Alice 再次把颜色做一次变换，把蓝色改成紫色，改绿色改成棕色，把橙色改成灰色，然后把所有的顶点盖上纸片。然后 Bob 再挑选一条边，比如像上图一样，选择的是一条竖着的边，然后让 Alice 揭开纸片看看，如果这时候 Bob 再次发现这条边两端的顶点颜色不同，那么 Bob 这时候已经有点动摇了，可能 Alice 真的有这个染色答案。可是，两次仍然不够，Bob 还想再多来几遍。那么经过反复多次重复这三个步骤，可以让 Alice 作弊并能成功骗过 Bob 的概率会以指数级的方式减小。假设经过 n 轮之后，Alice 作弊的概率为
这里 |E| 是图中所有边的个数， 如果 n 足够大，这个概率 Pr 会变得非常非常小，变得「微不足道」。可是，Bob 每次看到的局部染色情况都是 Alice 变换过后的结果，无论 Bob 看多少次，都不能拼出一个完整的三染色答案出来。实际上，Bob 在这个过程中，虽然获得了很多「信息」，但是却没有获得真正的「知识」。
信息 vs. 知识
信息 「Information」
知识 「Knowledge」
在地图三染色问题的交互证明中，当重复交互很多次之后，Bob 得到了大量的信息，但是这好比 Alice 发给 Bob 一堆随机数一样，Bob 并没有「知道」更多的东西。打个比方，如果 Alice 告诉 Bob 「1+1=2」，Bob 得到了这个信息，可是 Bob 并没有额外获取更多的「知识」，因为这个事实人人皆知。假如 Alice 告诉 Bob 2^2^41-1这个数是一个质数，很显然这个是「知识」，因为要算出来这个数是不是一个质数，这需要耗费大量的算力。假如 Alice 告诉 Bob，总共有两个顶点用了绿颜色，那么 Bob 就获得了宝贵的「知识」，因为基于他刚刚获取的这个信息，Bob 可以用更短的时间用一台图灵机去求解三染色问题。假如 Alice 又透露给 Bob，最左边的顶点颜色是用橙色，那么很显然，这个「信息」对于 Bob 求解问题并没有实质上的帮助。我们可以尝试定义一下，如果 Bob 在交互过程中获得的「信息」，可以帮助提升 Bob 直接破解 Alice 秘密的能力，那么我们说 Bob 「获得了知识」。由此可见，知识这个词的定义与 Bob 的计算能力相关，如果信息并不能增加 Bob 的计算能力，那么信息不能被称为「知识」。比如在 Alice 与 Bob 交互过程中，Alice 每次都掷一个硬币，然后告诉 Bob 结果，从信息角度看，Bob 得到的信息只是一个「事件」，然而 Bob 并没有得到任何「知识」，因为 Bob 完全可以自己来掷硬币。下面引用『Foundations of Cryptography—— Basic Tools』一书[10]中的总结
可以看到一个电路由很多个门组成，其中有加法门，还有乘法门。每一个门有几个输入引脚，有几个输出引脚。每一个门做一次加法运算，或乘法运算。别看这么简单，我们平时跑的（没有死循环）代码，都可以用算术电路来表示。这意味着什么呢？我们下面结合「零知识证明」与「电路可满足性问题」来试着解决数据的隐私保护问题。下面请思考一个场景：Bob 交给 Alice 一段代码 P，和一个输入 x，让 Alice 来运行一遍，然后把运行结果告诉 Bob。可能这个计算需要消耗资源，而 Bob 把计算过程外包给了 Alice。然后 Alice 运行了一遍，得到了结果 y。然后把 y 告诉 Bob。下面问题来了：
如何让 Bob 在不运行代码的前提下，相信代码 P 运行的结果一定是 y 呢？
这里是思考时间，大家可以想个五分钟 ……（五分钟后……）Alice 的一种做法是可以把整个计算过程用手机拍下来，这个视频里面包含了计算机 CPU，还有内存，在整个运行过程中的每一晶体管的状态。很显然这么做是不现实的。那么有没有更可行的方案呢？答案是 Bob 把程序 P 转换成一个完全等价的算术电路，然后把电路交给 Alice。Alice 只要计算这个电路就可以了，然后这个过程是可以用手机拍下来的，或者用纸记下来，如果电路规模没有那么大的话。Alice 只要把参数 6 输入到电路，然后记录下电路在运算过程中，所有与门相连的引脚线上的值。并且最后的电路输出引脚的值等于 y，那么 Bob 就能确信 Alice 确实进行了计算。Alice 需要把电路的所有门的输入与输出写到一张纸上，交给 Bob，这张纸就是一个计算证明。这样 Bob 完全可以在不重复计算电路的情况下来验证这张纸上的证明对不对，验证过程很简单：Bob 依次检查每一个门的输入输出能不能满足一个加法等式或者一个乘法等式。比如 1 号门是一个加法门，它的两个输入是 3，4，输出是7，那么很容易就知道这个门的计算是正确的。当 Bob 检查完所有的门之后，就能确信：Alice 确确实实进行了计算，没有作弊。这张纸上的内容就是「满足」算术电路 P 的一个解「Solution」。
对于 Alice 而言，Bob 如果用这种方式验证，她完全没有作弊的空间。但是这种方法很显然有个弊端：
弊端一：如果电路比较大，那么证明就很大，Bob 检查证明的工作量也很大。
弊端二：Bob 在验证过程中，知道了所有的电路运算细节，包括输入。
黑科技
我们再对刚才的 Alice 与 Bob 的场景做些修改。假如，Alice 自己还有一个秘密，比如说网银密码。而 Bob 想知道 Alice 的网银密码的长度是不是 20 位长。而 Alice 想了下，告诉他密码长度应该问题不大。这时候 Bob 把一个计算字符串长度的代码转换成了电路 Q，并且发给 Alice。Alice 用电路 Q 算了一下自己的密码，然后把电路所有门的引脚发给了 Bob，并带上运算结果 20。Wai……t，这是有问题的，Bob 拿到电路运算过程中的所有内部细节之后，不就知道密码了吗？是的，Alice 显然不能这么做。那么 Alice 应该怎么做？答案是有很多种办法，热爱区块链技术的读者最耳熟的就是 zkSNARK[11]，还有zkSTARK[12]，子弹证明BulletProof[13]，以及一些比较小众的技术，都可以帮 Alice 做到：
Alice 以一种零知识的方式，向 Bob 证明她计算过了电路，并且使用了她的秘密输入。
换句话说，这些「零知识的电路可满足性证明协议」为 Alice 提供了强大的武器来向 Bob 证明她的网银密码长度为 20，并且除此之外， Bob 再也得不到任何其它有用的信息。除了网银密码，Alice 理论上可以向 Bob 证明任何她的隐私数据的某些特性，但是并不暴露任何别的信息。
「零知识的电路可满足性证明协议」提供了一种最直接的保护隐私/敏感数据的技术
最近几年来，零知识证明构造技术发展日新月异，并且在区块链技术领域得到了越来越多的应用。最新的零知识证明技术，有的技术可以让 Bob 高速验证证明（在移动设备上几毫秒验证完成）；有的技术可以让所有吃瓜群众帮忙验证（非交互式零知识证明）；有的技术支持非常小的证明大小（小到几十个字节）。后续文章我们会逐步展开介绍。
[1] 西蒙, 辛格, 薛密. 费马大定理: 一个困惑了世间智者 358 年的谜[M]. 上海译文出版社, 1998.[2] Alec Wilkinson. The Pursuit of Beauty: Yitang Zhang solves a pure-math mystery. The New Yorker. Feb. 2015.[3] 马丁, 戴维斯, 张卜天. 逻辑的引擎[M]. 湖南科学技术出版社, 2012.[4] Raymond Smullyan. Gödel's Incompleteness Theorems, Oxford Univ.Press. 1991.[5] Turing, Alan. "On computable numbers, with an application to the Entscheidungsproblem." Proceedings of the London mathematical society 2.1 (1937): 230-265.[6] Pierce, Benjamin C., et al. "Software foundations." 中文译文: <https://github.com/Coq-zh/SF-zh[7] Kolata, Gina. "Computer math proof shows reasoning power." Math Horizons 4.3 (1997): 22-25.[8] Goldwasser, Shafi, Silvio Micali, and Charles Rackoff. "The knowledge complexity of interactive proof systems." SIAM Journal on computing 18.1 (1989): 186-208.[9] zkPoD: 区块链，零知识证明与形式化验证，实现无中介、零信任的公平交易. 安比实验室. 2019.[10] Oded, Goldreich. "Foundations of cryptography basic tools." (2001).[11] Gennaro, Rosario, et al. "Quadratic span programs and succinct NIZKs without PCPs." Annual International Conference on the Theory and Applications of Cryptographic Techniques. Springer Berlin, Heidelberg, 2013.[12] Ben-Sasson, Eli, et al. "Scalable, transparent, and post-quantum secure computational integrity." IACR Cryptology ePrint Archive 2018 (2018): 46.[13] Bünz, Benedikt, et al. "Bulletproofs: Short proofs for confidential transactions and more." 2018 IEEE Symposium on Security and Privacy (SP). IEEE, 2018